We present a method for verifying software transactional memory (STM) implementations. We decompose the problem by viewing STM descriptions at two levels: algorithm-level descriptions and actual implementations. The proof of serializability of the algorithm-level description, which is generic and performed manually, is separated from the proof that the implementation is a correct refinement of the algorithm-level description, which is checked mechanically.

In the algorithm-level proof for a lazy-invalidate, write-in-place STM, we model a program composed with an abstract STM, and devise a sufficient condition for serializability expressed as three intuitive properties. The implementation-level proof consists of checking whether these properties are satisfied by the STM implementation. We were able to express each check as an assertion in a particular *sequential* program that mimics interference between threads. This is a key benefit, as it allowed the assertion checks to be carried out using the sequential program verifier Boogie. We demonstrated our approach on a model of the Bartok STM.

Noteworthy additional work since the August 2007 MSR talk on this project includes the following:

1. A formal, algorithm-level model and semantics for programs using transactions. This model handles nested transactions, conflicts and rollbacks.
2. The definition of 'pure serializability', a correctness criterion for the kinds of programs described in (i).
3. A lower-level semantics that is at the same level of granularity as the actual STM implementation. This semantics also describes STM implementation state transitions that are invisible to the programmer.
4. A formalization of the desired relationship between implementation-level and algorithm-level executions. This includes translating sufficient conditions expressed at the algorithm-level to requirements at the implementation level.
5. The identification of abstractions in modeling required to make the refinement proof and algorithm-level serializability proof go through.

plus-circle Add Review

comment

Reviews